Theorem sylan2 286

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 277	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylan2.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 282	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  404  sylanr2  405  mpanr2  438  adantrl  478  adantrr  479  ancom2s  566  annimdc  939  3adantr1  1158  3adantr2  1159  3adantr3  1160  syl3anr1  1301  syl3anr3  1303  dfbi3dc  1408  xordidc  1410  elabgt  2893  sbciegft  3008  csbtt  3084  csbnestgf  3124  copsex2t  4260  pofun  4327  onsucmin  4521  onsucelsucr  4522  onsucsssucr  4523  ordsucunielexmid  4545  ordsuc  4577  nlimsucg  4580  elnn  4620  xpsspw  4753  elxp4  5131  elxp5  5132  funimass2  5310  imain  5314  funimaexg  5316  f1ff1  5445  dff1o2  5482  resdif  5499  funbrfv  5571  fvelimab  5589  eqfnfv2  5631  fvimacnvi  5647  ffvresb  5696  fnressn  5719  fmptapd  5724  fnex  5755  rexima  5772  ralima  5773  f1elima  5791  fnotovb  5935  mpoeq12  5952  fovcdm  6035  fnovrn  6040  ofrfval  6110  ofvalg  6111  cofunexg  6129  cofunex2g  6130  mpoexxg  6230  mpoexg  6231  f1o2ndf1  6248  spc2ed  6253  smodm2  6315  tfrlem9  6339  tfrlemibxssdm  6347  tfr1onlembxssdm  6363  tfrcllembxssdm  6376  tfri3  6387  rdgtfr  6394  rdgruledefgg  6395  oav2  6483  oasuc  6484  omv2  6485  onasuc  6486  omsuc  6492  onmsuc  6493  nnaass  6505  nndi  6506  nndir  6510  nnaword  6531  ecelqsg  6609  iinerm  6628  ecovass  6665  ecoviass  6666  ecovdi  6667  ecovidi  6668  fvdiagfn  6714  ixpssmap2g  6748  domentr  6812  xpdom1g  6854  fopwdom  6859  ssenen  6874  phplem3  6877  phplem4  6878  php5dom  6886  ssfilem  6898  diffitest  6910  ctssdccl  7135  pm54.43  7214  addclpi  7351  addasspig  7354  mulasspig  7356  distrpig  7357  mulcanpig  7359  nnppipi  7367  enqdc1  7386  addassnqg  7406  ltbtwnnqq  7439  prarloclemarch  7442  prarloclemarch2  7443  enq0sym  7456  enq0ref  7457  addclnq0  7475  nqpnq0nq  7477  nnanq0  7482  distrnq0  7483  addassnq0lemcl  7485  addassnq0  7486  distnq0r  7487  prarloclemlt  7517  genpassl  7548  genpassu  7549  genpassg  7550  nqpru  7576  addcomprg  7602  mulcomprg  7604  distrlem1prl  7606  distrlem1pru  7607  1idprl  7614  1idpru  7615  recexprlemdisj  7654  recexprlem1ssl  7657  peano2nnnn  7877  ax1rid  7901  axcaucvglemcl  7919  le2tri3i  8091  add4  8143  cnegexlem1  8157  cnegexlem3  8159  cnegex  8160  subadd  8185  addsub  8193  addsubeq4  8197  negdi  8239  renegcl  8243  resubcl  8246  subdi  8367  mulneg2  8378  mul2neg  8380  submul2  8381  ltnegcon2  8446  lenegcon2  8449  lesub0  8461  cru  8584  recextlem1  8633  recexap  8635  div12ap  8676  divnegap  8688  letrp1  8830  dfinfre  8938  peano2nn  8956  nndivre  8980  nnsub  8983  nndivtr  8986  arch  9198  bndndx  9200  nn0addge1  9247  nn0addge2  9248  zaddcl  9318  zsubcl  9319  zltnle  9324  zrevaddcl  9328  nzadd  9330  zleltp1  9333  zltlem1  9335  zdiv  9366  peano2uz2  9385  uzind  9389  eluzp1l  9577  ublbneg  9638  qaddcl  9660  qsubcl  9663  qreccl  9667  qdivcl  9668  qrevaddcl  9669  irradd  9671  irrmul  9672  rerpdivcl  9709  nn0ledivnn  9792  xrre  9845  rexsub  9878  xaddass  9894  xnpcan  9897  xsubge0  9906  xposdif  9907  elioc2  9961  icoshft  10015  iccdil  10023  fzss2  10089  fzsuc2  10104  fzrev2  10110  elfzm11  10116  elfzp1b  10122  fzrevral  10130  fzshftral  10133  fzof  10169  fzoval  10173  fzon  10191  fzosubel  10219  zpnn0elfzo  10232  elfzom1b  10254  qltnle  10271  flqlt  10309  flqbi  10316  flqaddz  10323  fzofig  10458  seq3feq2  10496  ser3le  10544  expp1  10553  expm1t  10574  expeq0  10577  binom2sub  10660  bernneq  10667  expnlbnd  10671  zzlesq  10715  faccl  10742  facdiv  10745  bcpasc  10773  bccl  10774  ffz0hash  10840  fnfzo0hash  10842  2shfti  10867  crim  10894  mulreap  10900  resub  10906  imsub  10914  ipcnval  10922  cjsub  10928  resqrexlemfp1  11045  resqrexlemgt0  11056  sqabsadd  11091  sqabssub  11092  abs2dif2  11143  cau3lem  11150  icodiamlt  11216  xrmaxaddlem  11295  clim  11316  clim2  11318  clim2c  11319  clim0c  11321  2clim  11336  climabs0  11342  climcn1  11343  climcn2  11344  climsqz  11370  climsqz2  11371  climub  11379  climserle  11380  fsum3cvg  11413  fisumss  11427  fsum3ser  11432  sumsplitdc  11467  fsump1i  11468  fsumlessfi  11495  telfsumo  11501  fsumparts  11505  iserabs  11510  binomlem  11518  isumsplit  11526  isum1p  11527  isumlessdc  11531  mertenslem2  11571  mertensabs  11572  prodfap0  11580  prodfrecap  11581  prodfdivap  11582  fproddccvg  11607  prodmodclem2  11612  fprodssdc  11625  fprodabs  11651  fprodeq0  11652  fprodeq0g  11673  ege2le3  11706  efsub  11716  efexp  11717  efsep  11726  sinsub  11775  cossub  11776  demoivre  11807  eirraplem  11811  moddvds  11833  0dvds  11845  iddvdsexp  11849  dvdssub  11872  dvdsle  11877  dvdsleabs  11878  dvdseq  11881  dvdsflip  11884  mulsucdiv2z  11917  divalgb  11957  divalg2  11958  ndvdsadd  11963  gcdneg  12010  gcdabs2  12018  modgcd  12019  bezoutlemsup  12037  gcdmultiplez  12049  gcdeq  12051  dvdssq  12059  lcmcllem  12094  lcmneg  12101  lcmdvds  12106  qredeu  12124  cncongrcoprm  12133  isprm3  12145  prmrp  12172  divnumden  12223  phiprmpw  12249  crth  12251  hashgcdlem  12265  hashgcdeq  12266  modprminv  12276  modprminveq  12277  modprmn0modprm0  12283  coprimeprodsq2  12285  pcpre1  12319  pccl  12326  pcmul  12328  pcdiv  12329  pcqcl  12333  pcexp  12336  pcdvds  12342  pcndvds  12344  pcndvds2  12346  pcelnn  12348  pcgcd1  12355  pc2dvds  12357  pc11  12358  gzsubcl  12407  4sqlem3  12417  setsresg  12545  xpsfeq  12814  submcl  12924  grpinvnzcl  13009  mulgnnass  13090  nmzsubg  13142  nmznsg  13145  resghm2b  13194  ghmnsgpreima  13201  iscrng2  13362  subrngpropd  13556  issubrg3  13587  subrgpropd  13588  islmodd  13602  lss1d  13692  lspsncl  13701  lspsnid  13716  df2idl2  13817  2idlcpbl  13832  iunopn  13939  unopn  13942  eltg  13989  eltg2  13990  tgcl  14001  tgiun  14010  tgidm  14011  isopn3i  14072  isneip  14083  neipsm  14091  restbasg  14105  restopn2  14120  lmbrf  14152  cnclima  14160  lmss  14183  txbasval  14204  txlm  14216  psmetxrge0  14269  blininf  14361  blssps  14364  blss  14365  elmopn2  14386  bdmet  14439  metrest  14443  bl2ioo  14479  dvcjbr  14609  efper  14665  sinperlem  14666  abssinper  14704  cxpexprp  14753  logcxp  14755  rpcxpcl  14761  rpcxproot  14771  rprelogbmulexp  14811  lgsval2lem  14849  lgssq2  14880  lgsprme0  14881  bj-inex  15097  peano5set  15130  findset  15135  bj-findis  15169  nninfsellemsuc  15200  nninfself  15201  cvgcmp2nlemabs  15219  iooref1o  15221  trilpolemeq1  15227  nconstwlpolemgt0  15251