Theorem sylan2 280

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

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

Assertion

Ref	Expression
sylan2	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 271	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylan2.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 276	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  sylan2b  281  sylan2br  282  syl2an  283  sylanr1  396  sylanr2  397  mpanr2  429  adantrl  462  adantrr  463  ancom2s  531  3adantr1  1098  3adantr2  1099  3adantr3  1100  syl3anr1  1222  syl3anr3  1224  dfbi3dc  1329  xordidc  1331  elabgt  2745  sbciegft  2855  csbtt  2929  csbnestgf  2965  copsex2t  4036  pofun  4103  onsucmin  4287  onsucelsucr  4288  onsucsssucr  4289  ordsucunielexmid  4310  ordsuc  4342  nlimsucg  4345  elnn  4383  xpsspw  4508  elxp4  4872  elxp5  4873  funimass2  5045  imain  5049  funimaexg  5051  f1ff1  5172  dff1o2  5206  resdif  5223  funbrfv  5288  fvelimab  5305  eqfnfv2  5343  fvimacnvi  5358  ffvresb  5403  fnressn  5425  fmptapd  5430  fnex  5459  rexima  5474  ralima  5475  f1elima  5492  fnotovb  5627  mpt2eq12  5644  fovrn  5722  fnovrn  5727  ofrfval  5799  fnofval  5800  cofunexg  5817  cofunex2g  5818  mpt2exxg  5912  mpt2exg  5913  f1o2ndf1  5928  spc2ed  5933  smodm2  5992  tfrlem9  6016  tfrlemibxssdm  6024  tfr1onlembxssdm  6040  tfrcllembxssdm  6053  tfri3  6064  rdgtfr  6071  rdgruledefgg  6072  oav2  6156  oasuc  6157  omv2  6158  onasuc  6159  omsuc  6165  onmsuc  6166  nnaass  6178  nndi  6179  nndir  6183  nnaword  6200  ecelqsg  6275  iinerm  6294  ecovass  6331  ecoviass  6332  ecovdi  6333  ecovidi  6334  fvdiagfn  6380  domentr  6438  xpdom1g  6479  fopwdom  6482  ssenen  6497  phplem3  6500  phplem4  6501  php5dom  6509  ssfilem  6521  diffitest  6533  pm54.43  6721  addclpi  6789  addasspig  6792  mulasspig  6794  distrpig  6795  mulcanpig  6797  nnppipi  6805  enqdc1  6824  addassnqg  6844  ltbtwnnqq  6877  prarloclemarch  6880  prarloclemarch2  6881  enq0sym  6894  enq0ref  6895  addclnq0  6913  nqpnq0nq  6915  nnanq0  6920  distrnq0  6921  addassnq0lemcl  6923  addassnq0  6924  distnq0r  6925  prarloclemlt  6955  genpassl  6986  genpassu  6987  genpassg  6988  nqpru  7014  addcomprg  7040  mulcomprg  7042  distrlem1prl  7044  distrlem1pru  7045  1idprl  7052  1idpru  7053  recexprlemdisj  7092  recexprlem1ssl  7095  peano2nnnn  7293  ax1rid  7315  axcaucvglemcl  7333  le2tri3i  7496  add4  7546  cnegexlem1  7560  cnegexlem3  7562  cnegex  7563  subadd  7588  addsub  7596  addsubeq4  7600  negdi  7642  renegcl  7646  resubcl  7649  subdi  7766  mulneg2  7777  mul2neg  7779  submul2  7780  ltnegcon2  7845  lenegcon2  7848  lesub0  7860  cru  7979  recextlem1  8018  recexap  8020  div12ap  8059  divnegap  8071  letrp1  8203  dfinfre  8311  peano2nn  8328  nndivre  8351  nnsub  8354  nndivtr  8357  arch  8562  bndndx  8564  nn0addge1  8611  nn0addge2  8612  zaddcl  8686  zsubcl  8687  zltnle  8692  zrevaddcl  8696  nzadd  8698  zleltp1  8701  zltlem1  8703  zdiv  8730  peano2uz2  8749  uzind  8753  eluzp1l  8938  ublbneg  8993  qaddcl  9015  qsubcl  9018  qreccl  9022  qdivcl  9023  qrevaddcl  9024  irradd  9026  irrmul  9027  rerpdivcl  9059  nn0ledivnn  9133  xrre  9177  elioc2  9249  icoshft  9302  iccdil  9310  fzss2  9372  fzsuc2  9386  fzrev2  9392  elfzm11  9398  elfzp1b  9404  fzrevral  9412  fzshftral  9415  fzof  9445  fzoval  9449  fzon  9466  fzosubel  9494  zpnn0elfzo  9507  elfzom1b  9529  qltnle  9546  flqlt  9579  flqbi  9586  flqaddz  9593  fzofig  9728  iseqfeq2  9764  iseqfeq  9766  iseqsplit  9773  expp1  9799  expm1t  9820  expeq0  9823  binom2sub  9903  bernneq  9909  expnlbnd  9913  faccl  9978  facdiv  9981  bcpasc  10009  bccl  10010  ffz0hash  10072  fnfzo0hash  10074  2shfti  10093  crim  10119  mulreap  10125  resub  10131  imsub  10139  ipcnval  10147  cjsub  10153  resqrexlemfp1  10269  resqrexlemgt0  10280  sqabsadd  10315  sqabssub  10316  abs2dif2  10367  cau3lem  10374  icodiamlt  10440  clim  10494  clim2  10496  clim2c  10497  clim0c  10499  2clim  10514  climabs0  10520  climcn1  10521  climcn2  10522  climsqz  10547  climsqz2  10548  climub  10556  climserile  10557  fisumcvg  10574  moddvds  10585  0dvds  10596  iddvdsexp  10600  dvdssub  10621  dvdsle  10625  dvdsleabs  10626  dvdseq  10629  dvdsflip  10632  mulsucdiv2z  10665  divalgb  10705  divalg2  10706  ndvdsadd  10711  gcdneg  10753  gcdabs2  10761  modgcd  10762  bezoutlemsup  10778  gcdmultiplez  10790  gcdeq  10792  dvdssq  10800  lcmcllem  10829  lcmneg  10836  lcmdvds  10841  qredeu  10859  cncongrcoprm  10868  isprm3  10880  prmrp  10904  divnumden  10954  phiprmpw  10978  crth  10980  hashgcdlem  10983  hashgcdeq  10984  bj-inex  11141  peano5set  11178  findset  11183  bj-findis  11217  nninfsellemsuc  11246  nninfself  11247