Theorem expcom 109

Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
exp.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
expcom	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 108	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 27	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  ancoms  255  syldan  266  sylan  267  pm4.79dc  809  dedlema  876  dedlemb  877  19.35-1  1515  cbval2  1796  cbvex2  1797  r19.21be  2410  r19.35-1  2460  mosubt  2718  sbcrext  2835  uneqdifeqim  3308  ssuni  3602  uniss2  3611  elpwuni  3741  elssabg  3902  elpw2g  3910  epelg  4027  elnn  4328  relop  4486  riinint  4593  cnviinm  4859  funopg  4934  fun  5063  tz6.12c  5203  fvelrnb  5221  fmptco  5330  fnressn  5349  fressnfv  5350  fvtp2g  5370  fvtp3g  5371  fconst2g  5376  isores3  5455  isoselem  5459  eloprabga  5591  fo1stresm  5788  poxp  5853  brtpos2  5866  smores  5907  tfrlem1  5923  tfrlemi1  5946  rdgon  5973  frecrdg  5992  freccl  5993  nnacl  6059  nnmcl  6060  nnacom  6063  nnaass  6064  nnmsucr  6067  nnmordi  6089  iinerm  6178  th3qlem2  6209  brdomg  6229  f1domg  6238  ssdomg  6258  nndomo  6326  carden2bex  6369  addclpi  6425  addnidpig  6434  genpassl  6622  genpassu  6623  nqprloc  6643  ltaprlem  6716  recexprlemopl  6723  recexprlemopu  6725  recexprlemupu  6726  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemupu  6747  caucvgprlemupu  6770  caucvgprprlemupu  6798  archsr  6866  peano2nnnn  6929  receuap  7650  peano2nn  7926  nnaddcl  7934  zrevaddcl  8295  zdiv  8328  nneo  8341  zeo2  8344  peano5uzti  8346  fzind  8353  fnn0ind  8354  lbzbi  8551  qrevaddcl  8578  irradd  8580  irrmul  8581  ltsubrp  8617  ltaddrp  8618  icoshft  8858  fzen  8907  elfzm11  8953  uzsplit  8954  fzoval  9005  elfzom1elp1fzo  9058  frec2uzzd  9186  frec2uzrdg  9195  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  iseqcaopr3  9240  iseqid3s  9246  iseqhomo  9248  expadd  9297  expmul  9300  leexp1a  9309  shftlem  9417  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc3  9614  climub  9864  climserile  9865  nn0seqcvgd  9880  ialginv  9886  ialgcvga  9890  ialgfx  9891  2spim  9906