Theorem adantrd 494

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

Ref	Expression
adantrd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
adantrd	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 485	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 398

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  im2anan9  628  jaoa  966  prlem1  1063  cad0  1628  dfsb1  2502  unineq  4231  dfopif  4818  elssabg  5289  exopxfr2  5805  tz7.7  6357  oneqmini  6384  fvun1  6943  fconst5  7175  fpropnf1  7236  f1ounsn  7241  isomin  7306  isofrlem  7309  poxp  8092  poseq  8122  tposfo2  8213  onfununi  8296  tfrlem9a  8341  oecl  8490  oawordri  8503  omwordri  8525  odi  8532  pssnn  9122  prdom2  9948  acni2  9988  cardinfima  10039  cfslb2n  10211  infpssrlem4  10249  axdc3lem4  10396  brdom6disj  10475  tskr1om  10711  indpi  10851  1idpr  10973  1re  11167  mulge0  11691  infm3  12137  uzind  12651  suprfinzcl  12673  uzwo  12898  xrlttr  13128  xmullem2  13254  snunico  13469  fzen  13532  fz0fzelfz0  13625  sqlecan  14208  hashf1lem2  14455  ccatsymb  14582  lo1le  15651  fsumss  15724  ntrivcvgfvn0  15901  fprodss  15950  smupvallem  16489  zeqzmulgcd  16516  lcmgcdlem  16612  lcmdvds  16614  lcmfunsnlem2lem1  16644  coprmproddvdslem  16668  cncongr2  16674  exprmfct  16711  infpnlem1  16918  prmdvdsprmop  17051  prmgaplem7  17065  prmlem0  17113  sscfn2  17823  isssc  17825  iszeroi  18014  funcsetcestrclem8  18166  dirge  18607  efgval  19729  dmdprd  20012  dprdw  20024  rhmsubclem4  20706  lpigen  21374  psrbaglefi  21947  matvscl  22460  scmatghm  22562  slesolinv  22709  cpmatacl  22745  pnfnei  23249  mnfnei  23250  cmpcld  23431  isfildlem  23886  metrest  24553  blval2  24591  iscmet3lem2  25323  ivthlem3  25484  mbfi1fseqlem4  25749  itg2seq  25773  aalioulem6  26367  taylthlem2  26403  chpchtsum  27249  dchrmulcl  27279  bcmono  27307  nosupno  27733  nosupbday  27735  noinfno  27748  noinfbday  27750  nocvxminlem  27813  cuteq1  27876  oncutlt  28323  oniso  28330  bdayn0p1  28428  bdayfinbndlem2  28527  z12sge0  28542  cgrg3col4  28988  brbtwn2  29041  axeuclid  29099  umgredg  29274  pthdivtx  29862  pthdlem1  29901  shsvs  31461  cnlnssadj  32218  atexch  32519  mdsymlem5  32545  disjxpin  32726  fldextrspunlsplem  33914  sigaclci  34373  fnrelpredd  35332  satfv0  35646  satffunlem2lem1  35692  dmopab3rexdif  35693  elfuns  36201  altopth1  36253  btwnexch2  36311  ifscgr  36332  colinbtwnle  36406  trer  36614  elicc3  36615  bj-imdirval3  37614  bj-finsumval0  37715  difunieq  37806  fvineqsneu  37843  fvineqsneq  37844  poimirlem27  38084  poimir  38090  cnambfre  38105  itg2addnclem2  38109  itg2addnc  38111  areacirclem1  38145  heiborlem4  38251  elghomlem2OLD  38323  rngo2  38344  ispridl2  38475  ispridlc  38507  iss2  38781  membpartlem19  39351  paddasslem14  40395  ispsubcl2N  40509  cdleme29ex  40936  cdlemefr29exN  40964  eldiophss  43293  rencldnfilem  43335  oaabsb  43809  cantnfresb  43839  tfsconcatrn  43857  naddwordnexlem1  43912  clsk1indlem3  44557  ntrneikb  44608  mnuop3d  44785  ax6e2ndeq  45073  suctrALT2  45350  relpmin  45466  relpfrlem  45467  2reu3  47642  iccpartiltu  47966  bgoldbtbndlem2  48366  grtrimap  48508  grimgrtri  48509  isubgr3stgrlem6  48531  isubgr3stgr  48535  pgnbgreunbgrlem1  48673  pgnbgreunbgrlem4  48679  itschlc0xyqsol1  49326  resipos  49534  elsetrecslem  50258  aacllem  50360