Theorem expcom 114

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 113	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 30	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  ancoms  264  syldan  276  sylan  277  pm4.79dc  845  dedlema  913  dedlemb  914  19.35-1  1558  cbval2  1841  cbvex2  1842  nelelne  2343  r19.21be  2460  r19.35-1  2513  mosubt  2783  sbcrext  2905  uneqdifeqim  3355  ssuni  3658  uniss2  3667  elpwuni  3797  elssabg  3959  elpw2g  3967  epelg  4091  elnn  4393  relop  4554  riinint  4662  cnviinm  4938  funopg  5013  fun  5147  tz6.12c  5297  fvelrnb  5315  fmptco  5427  fnressn  5446  fressnfv  5447  fvtp2g  5467  fvtp3g  5468  fconst2g  5473  isores3  5555  isoselem  5560  eloprabga  5692  fo1stresm  5889  poxp  5954  brtpos2  5970  smores  6011  tfrlem1  6027  tfrlemi1  6051  tfr1onlemaccex  6067  tfrcllemaccex  6080  frecrdg  6127  oawordriexmid  6185  nnacl  6195  nnmcl  6196  nnacom  6199  nnaass  6200  nnmsucr  6203  nndifsnid  6218  nnmordi  6227  iinerm  6316  th3qlem2  6347  elpmg  6373  pmss12g  6384  mapsn  6399  brdomg  6417  f1domg  6427  ssdomg  6447  nndomo  6532  carden2bex  6761  addclpi  6830  addnidpig  6839  genpassl  7027  genpassu  7028  nqprloc  7048  ltaprlem  7121  recexprlemopl  7128  recexprlemopu  7130  recexprlemupu  7131  recexprlemss1l  7138  recexprlemss1u  7139  cauappcvgprlemupu  7152  caucvgprlemupu  7175  caucvgprprlemupu  7203  archsr  7271  peano2nnnn  7334  receuap  8077  peano2nn  8369  nnaddcl  8377  zrevaddcl  8733  nzadd  8735  zdiv  8767  nneo  8782  zeo2  8785  peano5uzti  8787  fzind  8794  fnn0ind  8795  lbzbi  9033  qrevaddcl  9061  irradd  9063  irrmul  9064  ltsubrp  9100  ltaddrp  9101  icoshft  9339  fzen  9389  elfzm11  9435  uzsplit  9436  fzoval  9487  elfzom1elp1fzo  9541  exfzdc  9579  modaddmodup  9722  frec2uzrdg  9744  iseqoveq  9798  iseqss  9799  iseqsst  9800  iseqfveq2  9802  iseqshft2  9806  monoord  9809  iseqsplit  9812  iseqcaopr3  9814  iseqf1olemp  9835  iseqid3s  9841  iseqid2  9843  iseqhomo  9844  iseqz  9845  expadd  9895  expmul  9898  leexp1a  9908  faccl  10039  facdiv  10042  faclbnd  10045  faclbnd6  10048  omgadd  10106  hashunsng  10111  iseqcoll  10143  shftlem  10146  resqrexlemover  10338  resqrexlemdecn  10340  resqrexlemlo  10341  resqrexlemcalc3  10344  climub  10624  climserile  10625  dvds2ln  10704  dvdsabseq  10723  dvdsdivcl  10726  alzdvds  10730  oddnn02np1  10755  m1exp1  10776  nn0o1gt2  10780  nno  10781  ndvdsadd  10806  flodddiv4  10809  gcddiv  10883  gcdmultiple  10884  gcdmultiplez  10885  rplpwr  10891  dvdssq  10895  nn0seqcvgd  10898  ialginv  10904  ialgcvga  10908  ialgfx  10909  isprm2  10974  isprm3  10975  prmdvdsexp  11002  2spim  11105