Theorem syl5com 32

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 26	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 31	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  33  syl5  35  speimfw  1993  axc16i  2468  eupickbi  2664  ceqsalgALT  3491  cgsexg  3499  cgsex2g  3500  cgsex4g  3501  spcegv  3557  spc2egv  3559  disjne  4416  uneqdifeq  4454  preqsnd  4825  preq12nebg  4829  opthprneg  4831  dfiun2g  4995  axprlem4  5399  pocl  5579  relresfld  6279  unixpid  6287  ordnbtwn  6458  sucssel  6460  ordelinel  6466  funmo  6554  fvimacnv  7050  ordsuc  7811  tfi  7850  focdmex  7954  f1ovv  7956  opreuopreu  8032  frrlem4  8287  tz7.49  8433  oeworde  8580  fsetprcnex  8860  dom2d  8991  findcard  9149  fisupg  9249  dffi3  9392  noinfep  9630  cantnflem2  9660  ttrcltr  9686  tcmin  9709  rankr1ag  9775  rankunb  9823  rankxpsuc  9855  alephordi  10059  alephsucdom  10064  alephinit  10080  dfac9  10121  ackbij2lem4  10225  cff1  10243  cfslbn  10252  cfcoflem  10257  cfcof  10259  infpssrlem5  10292  isfin7-2  10381  acncc  10425  domtriomlem  10427  axdc3lem2  10436  ttukeylem1  10494  iundom2g  10525  axpowndlem3  10585  wunex2  10724  grupr  10783  gruiun  10785  eltskm  10829  nqereu  10915  addcanpr  11032  axpre-sup  11155  relin01  11739  nneo  12681  zeo2  12684  xrub  13339  uznfz  13640  difelfzle  13671  ssfzo12  13790  facndiv  14326  hashgt12el2  14462  hash2prde  14509  hash2pwpr  14515  hashle2prv  14517  tpfo  14539  fi1uzind  14546  swrdswrd  14744  pfxccatin12lem2  14770  pfxccatin12  14772  pfxccat3  14773  cshwidxmod  14842  2cshwcshw  14864  fsumcom2  15827  fprodss  16004  fprodcom2  16040  sumodd  16447  ndvdssub  16468  eucalglt  16644  prmind2  16744  coprm  16771  prmdiveq  16846  prmdvdsprmop  17104  prmgaplem5  17116  cicsym  17862  drsdir  18359  lublecllem  18415  istos  18473  tsrlin  18642  dirge  18660  mhmlin  18852  issubg2  19209  nsgbi  19224  symgextf1lem  19491  sylow2a  19690  gsumpr  20026  0ringnnzr  20610  0ring01eq  20614  01eq0ringOLD  20616  nrhmzr  20623  issubrng2  20644  issubrg2  20678  abvmul  20905  abvtri  20906  lmodlema  20967  rmodislmodlem  21031  rmodislmod  21032  ellspsn6  21096  lmhmlin  21137  lbsind  21182  isprmidlc  21453  nzerooringczr  21611  ipcj  21765  obsip  21852  lindsss  21955  mamufacex  22534  mavmulsolcl  22689  slesolvec  22817  inopn  23037  basis1  23088  tgss  23106  tgcl  23107  elcls3  23221  neindisj2  23261  cncls  23412  1stcelcls  23599  qtoptop2  23837  nrmr0reg  23887  fbasssin  23974  fbfinnfr  23979  fbunfip  24007  filufint  24058  uffix  24059  ufinffr  24067  ufilen  24068  fmfnfmlem1  24092  flftg  24134  alexsubALT  24189  xmeteq0  24476  blssexps  24564  blssex  24565  mopni3  24632  neibl  24639  metss  24646  metcnp3  24678  nmvs  24814  iccntr  24960  reconnlem2  24966  lebnumlem3  25103  caubl  25448  bcthlem5  25468  ovolunlem1  25637  voliunlem1  25690  volsuplem  25695  ellimc3  26019  logbgcd1irr  26940  lgsqrmodndvds  27498  gausslemma2dlem0i  27509  2lgsoddprmlem3  27559  dchrisumlema  27633  nofv  27802  nolesgn2o  27816  nogesgn1o  27818  nosupbnd1lem5  27857  addsprop  28150  negsprop  28209  mulsprop  28304  precsexlem6  28386  precsexlem7  28387  umgrnloopv  29437  usgrnloopvALT  29532  umgrres1lem  29641  upgrres1  29644  nbuhgr  29674  cplgrop  29768  fusgrregdegfi  29900  g0wlk0  29981  wlkdlem2  30012  upgrwlkdvdelem  30066  crctcshwlkn0lem3  30142  crctcshwlkn0lem5  30144  wspn0  30254  usgrwwlks2on  30288  umgrwwlks2on  30289  elwspths2spth  30300  clwlkclwwlklem2a  30330  clwlkclwwlklem3  30333  clwwlkn1loopb  30375  clwwlknonwwlknonb  30438  clwwlknonex2lem2  30440  3cyclfrgrrn2  30619  frgrncvvdeqlem8  30638  frgrwopregasn  30648  frgrwopregbsn  30649  frgrwopreg1  30650  frgrwopreg2  30651  frgrregord013  30727  frgrogt3nreg  30729  ablocom  30881  ubthlem1  31203  shaddcl  31550  shmulcl  31551  spansnss2  31908  cnopc  32246  cnfnc  32263  adj1  32266  pjorthcoi  32502  stj  32568  mdsl1i  32654  chirredlem1  32723  mdsymlem5  32740  cdj3lem2b  32770  slmdlema  33504  vonf1oonfo  35580  pconncn  35697  cvmlift2lem1  35775  fmla0xp  35856  ss2mcls  36041  antnestlaw2  36165  dfon2lem6  36259  waj-ax  36906  lukshef-ax2  36907  tr0elw  36976  bj-alrim  37299  bj-nexdt  37303  sucneqond  37992  rdgssun  38005  ptrecube  38252  poimirlem26  38278  poimirlem29  38281  heiborlem1  38443  rngodm1dm2  38564  rngoueqz  38572  zerdivemp1x  38579  isdrngo3  38591  0rngo  38659  pridl  38669  ispridlc  38702  isdmn3  38706  dmnnzd  38707  elrelscnveq3  39257  lshpcmp  39743  omllaw  39998  dochexmidlem7  42221  lspindp5  42525  zdivgd  43079  fsuppind  43305  dfac21  43776  eexinst11  45219  ax6e2eq  45249  e222  45328  e111  45366  e333  45424  natlocalincr  47575  imarnf1pr  48002  2ffzoeq  48048  iccpartigtl  48155  iccpartgt  48159  lighneallem3  48342  lighneal  48346  requad1  48370  evenltle  48465  fppr2odd  48479  sgoldbeven3prm  48531  bgoldbtbndlem2  48554  isubgr3stgrlem4  48717  isubgr3stgrlem7  48720  gpgedg2iv  48815  isidom3  49093  idomnzd  49094  lincdifsn  49187  lindslinindimp2lem4  49224  snlindsntor  49234  lincresunit3lem1  49242  lincresunit3lem2  49243  f002  49615  setrec1lem2  50449