Theorem adantrd 491

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 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9  621  jaoa  958  prlem1  1055  cad0  1620  dfsb1  2486  unineq  4229  dfopif  4814  elssabg  5281  exopxfr2  5794  tz7.7  6344  oneqmini  6371  fvun1  6926  fconst5  7155  fpropnf1  7216  f1ounsn  7221  isomin  7286  isofrlem  7289  poxp  8072  poseq  8102  tposfo2  8193  onfununi  8275  tfrlem9a  8319  oecl  8466  oawordri  8479  omwordri  8501  odi  8508  pssnn  9097  prdom2  9922  acni2  9962  cardinfima  10013  cfslb2n  10184  infpssrlem4  10222  axdc3lem4  10369  brdom6disj  10448  tskr1om  10684  indpi  10824  1idpr  10946  1re  11138  mulge0  11662  infm3  12109  uzind  12615  suprfinzcl  12637  uzwo  12855  xrlttr  13085  xmullem2  13211  snunico  13426  fzen  13489  fz0fzelfz0  13582  sqlecan  14165  hashf1lem2  14412  ccatsymb  14539  lo1le  15608  fsumss  15681  ntrivcvgfvn0  15858  fprodss  15907  smupvallem  16446  zeqzmulgcd  16473  lcmgcdlem  16569  lcmdvds  16571  lcmfunsnlem2lem1  16601  coprmproddvdslem  16625  cncongr2  16631  exprmfct  16668  infpnlem1  16875  prmdvdsprmop  17008  prmgaplem7  17022  prmlem0  17070  sscfn2  17779  isssc  17781  iszeroi  17970  funcsetcestrclem8  18122  dirge  18563  efgval  19686  dmdprd  19969  dprdw  19981  rhmsubclem4  20659  lpigen  21328  psrbaglefi  21919  matvscl  22409  scmatghm  22511  slesolinv  22658  cpmatacl  22694  pnfnei  23198  mnfnei  23199  cmpcld  23380  isfildlem  23835  metrest  24502  blval2  24540  iscmet3lem2  25272  ivthlem3  25433  mbfi1fseqlem4  25698  itg2seq  25722  aalioulem6  26317  taylthlem2  26354  chpchtsum  27199  dchrmulcl  27229  bcmono  27257  nosupno  27684  nosupbday  27686  noinfno  27699  noinfbday  27701  nocvxminlem  27763  cuteq1  27826  oncutlt  28273  oniso  28280  bdayn0p1  28378  bdayfinbndlem2  28477  z12sge0  28492  cgrg3col4  28938  brbtwn2  28991  axeuclid  29049  umgredg  29224  pthdivtx  29813  pthdlem1  29852  shsvs  31412  cnlnssadj  32169  atexch  32470  mdsymlem5  32496  disjxpin  32676  fldextrspunlsplem  33836  sigaclci  34295  fnrelpredd  35253  satfv0  35559  satffunlem2lem1  35605  dmopab3rexdif  35606  elfuns  36114  altopth1  36166  btwnexch2  36224  ifscgr  36245  colinbtwnle  36319  trer  36517  elicc3  36518  bj-imdirval3  37517  bj-finsumval0  37618  difunieq  37707  fvineqsneu  37744  fvineqsneq  37745  poimirlem27  37985  poimir  37991  cnambfre  38006  itg2addnclem2  38010  itg2addnc  38012  areacirclem1  38046  heiborlem4  38152  elghomlem2OLD  38224  rngo2  38245  ispridl2  38376  ispridlc  38408  iss2  38682  membpartlem19  39252  paddasslem14  40296  ispsubcl2N  40410  cdleme29ex  40837  cdlemefr29exN  40865  eldiophss  43223  rencldnfilem  43269  oaabsb  43743  cantnfresb  43773  tfsconcatrn  43791  naddwordnexlem1  43846  clsk1indlem3  44491  ntrneikb  44542  mnuop3d  44719  ax6e2ndeq  45007  suctrALT2  45284  relpmin  45400  relpfrlem  45401  2reu3  47573  iccpartiltu  47897  bgoldbtbndlem2  48297  grtrimap  48439  grimgrtri  48440  isubgr3stgrlem6  48462  isubgr3stgr  48466  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  itschlc0xyqsol1  49257  resipos  49465  elsetrecslem  50189  aacllem  50291