Theorem syl5com 31

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

Hypotheses

Ref	Expression
syl5com.1	⊢ (𝜑 → 𝜓)
syl5com.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5com	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 30	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4

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

This theorem is referenced by:  com12  32  syl5  34  speimfw  2057  axc16i  2486  eupickbi  2714  ceqsalgALT  3436  cgsexg  3443  cgsex2g  3444  cgsex4g  3445  spc2egv  3499  spc3egv  3501  disjne  4230  uneqdifeq  4264  preqsnd  4590  preq12nebg  4596  opthprneg  4598  relresfld  5890  unixpid  5898  ordnbtwn  6041  sucssel  6043  ordelinel  6049  fvimacnv  6564  2f1fvneq  6751  ordsuc  7254  tfi  7293  fornex  7375  f1ovv  7377  wfrlem4  7663  wfrlem4OLD  7664  wfrlem10  7670  tz7.49  7786  oeworde  7920  dom2d  8243  findcard  8448  fisupg  8457  dffi3  8586  fiinfg  8654  noinfep  8814  cantnflem2  8844  tcmin  8874  rankr1ag  8922  rankelb  8944  rankunb  8970  rankxpsuc  9002  alephordi  9190  alephsucdom  9195  alephinit  9211  dfac9  9253  ackbij2lem4  9359  cff1  9375  cfslbn  9384  cfcoflem  9389  cfcof  9391  infpssrlem5  9424  isfin7-2  9513  acncc  9557  domtriomlem  9559  axdc3lem2  9568  ttukeylem1  9626  iundom2g  9657  axpowndlem3  9716  wunex2  9855  grupr  9914  gruiun  9916  eltskm  9960  nqereu  10046  addcanpr  10163  axpre-sup  10285  relin01  10847  nneo  11747  zeo2  11750  xrub  12380  uznfz  12666  difelfzle  12696  ssfzo12  12805  facndiv  13315  hashgt12el2  13448  hash2prde  13489  hash2pwpr  13495  hashle2prv  13497  fi1uzind  13516  swrdswrd  13704  swrdccatin2  13731  swrdccatin12lem2  13733  swrdccatin12  13735  swrdccat3  13736  swrdccatid  13741  repswswrd  13775  2cshwcshw  13815  relexpcnvd  14019  relexpdmd  14027  relexprnd  14031  relexpfldd  14033  relexpaddd  14037  fsumcom2  14748  fprodss  14919  fprodcom2  14955  sumodd  15351  ndvdssub  15372  eucalglt  15537  prmind2  15636  coprm  15660  prmdiveq  15728  prmdvdsprmop  15984  prmgaplem5  15996  drsdir  17160  lublecllem  17213  istos  17260  tsrlin  17444  dirge  17462  mhmlin  17567  issubg2  17831  nsgbi  17847  symgextf1lem  18061  sylow2a  18255  issubrg2  19024  abvmul  19053  abvtri  19054  lmodlema  19092  rmodislmodlem  19154  rmodislmod  19155  lspsnel6  19221  lmhmlin  19262  lbsind  19307  0ring01eq  19500  01eq0ring  19501  ipcj  20209  obsip  20296  lindsss  20394  mamufacex  20426  mavmulsolcl  20589  slesolvec  20718  inopn  20938  basis1  20989  tgss  21007  tgcl  21008  elcls3  21122  neindisj2  21162  cncls  21313  1stcelcls  21499  qtoptop2  21737  nrmr0reg  21787  fbasssin  21874  fbfinnfr  21879  fbunfip  21907  filufint  21958  uffix  21959  ufinffr  21967  ufilen  21968  fmfnfmlem1  21992  flftg  22034  alexsubALT  22089  xmeteq0  22377  blssexps  22465  blssex  22466  mopni3  22533  neibl  22540  metss  22547  metcnp3  22579  nmvs  22714  reperflem  22855  iccntr  22858  reconnlem2  22864  lebnumlem3  22996  caubl  23340  bcthlem5  23359  ovolunlem1  23501  voliunlem1  23554  volsuplem  23559  ellimc3  23880  lhop1lem  24013  ulmss  24388  lgsqrmodndvds  25315  2lgsoddprmlem3  25376  dchrisumlema  25414  umgrnloopv  26238  usgrnloopvALT  26331  umgrres1lem  26441  upgrres1  26444  nbuhgr  26478  cplgrop  26584  fusgrregdegfi  26716  g0wlk0  26799  wlkdlem2  26831  upgrwlkdvdelem  26883  crctcshwlkn0lem4  26957  crctcshwlkn0lem5  26958  wspn0  27087  umgrwwlks2on  27121  elwspths2spth  27132  clwlkclwwlklem2a  27164  clwlkclwwlklem3  27167  clwwlkn1loopb  27215  clwlksfclwwlkOLD  27259  clwwlknonex2lem2  27300  3cyclfrgrrn2  27485  frgrncvvdeqlem8  27504  frgrwopregasn  27514  frgrwopregbsn  27515  frgrwopreg1  27516  frgrwopreg2  27517  frgrregord013  27606  frgrogt3nreg  27608  ablocom  27754  ubthlem1  28077  shaddcl  28425  shmulcl  28426  spansnss2  28785  cnopc  29123  cnfnc  29140  adj1  29143  pjorthcoi  29379  stj  29445  mdsl1i  29531  chirredlem1  29600  mdsymlem5  29617  cdj3lem2b  29647  slmdlema  30104  pconncn  31551  cvmlift2lem1  31629  ss2mcls  31810  dfon2lem6  32035  frrlem4  32126  nofv  32153  nolesgn2o  32167  nosupbnd1lem5  32201  nn0prpw  32661  waj-ax  32752  lukshef-ax2  32753  bj-alrim  33020  bj-nexdt  33024  sucneqond  33548  ptrecube  33741  poimirlem26  33767  poimirlem29  33770  heiborlem1  33940  rngodm1dm2  34061  rngoueqz  34069  zerdivemp1x  34076  isdrngo3  34088  0rngo  34156  pridl  34166  ispridlc  34199  isdmn3  34203  dmnnzd  34204  elrelscnveq3  34573  lshpcmp  34787  omllaw  35042  dochexmidlem7  37265  lspindp5  37569  dfac21  38155  eexinst11  39249  ax6e2eq  39289  e222  39377  e111  39415  e333  39475  imarnf1pr  41890  2ffzoeq  41931  iccpartigtl  41952  iccpartgt  41956  pfxccatin12lem2  42017  pfxccatin12  42018  pfxccat3  42019  lighneallem3  42117  lighneal  42121  evenltle  42219  sgoldbeven3prm  42264  bgoldbtbndlem2  42287  nrhmzr  42459  nzerooringczr  42658  gsumpr  42725  lincdifsn  42799  snlindsntor  42846  lincresunit3lem1  42854  lincresunit3lem2  42855  lincresunit3  42856  setrec1lem2  43021